Nuprl Lemma : rcv?-link
0,22
postcript
pdf
E
,
X1
,
X2
:Type,
info
:(
E
(Id
X1
+(IdLnk
E
)
X2
)),
e
:
E
. rcv?(
e
)
(link(
e
) ~ lnk(kind(
e
)))
latex
Definitions
True
,
t
T
,
IdLnk
,
x
:
A
B
(
x
)
,
x
.
A
(
x
)
,
x
:
A
.
B
(
x
)
,
x
.
t
(
x
)
,
1of(
t
)
,
P
Q
,
False
,
b
,
lnk(
k
)
,
rcv(
l
,
tg
)
,
left
+
right
,
Id
,
f
(
a
)
,
x
:
A
B
(
x
)
,
s
=
t
,
ecase1(
e
;
info
;
i
.
f
(
i
);
l
,
e'
.
g
(
l
;
e'
))
,
kind(
e
)
,
link(
e
)
,
rcv?(
e
)
,
Type
,
<
a
,
b
>
,
{
T
}
,
SQType(
T
)
,
s
~
t
Lemmas
IdLnk
sq
,
assert
wf
,
rcv?
wf
,
Id
wf
,
false
wf
,
pi1
wf
,
IdLnk
wf
,
true
wf
origin
E, X1, X2:Type, info:(E
(Id
X1+(IdLnkE)X2)), e:E. rcv?(e) 
(link(e) ~ lnk(kind(e))) E, X1, X2:Type, info:(E(IdX1+(IdLnkE)X2)), e:E. rcv?(e) (link(e) ~ lnk(kind(e))) 
TB(x)
x.A(x)x:A. B(x)
x. t(x) Q
bB(x)